A:es_realizer{i:l}. 
(Rplus?(A))
 guard(((R-size(Rplus-left(A)) < R-size(A))  (R-size(Rplus-right(A)) < R-size(A)))) 

latex

Definitions	if b then t else f fi , ff, t  T, x. t(x), prop{i:l}, Rplus-right(x1), Rplus-left(x1), R-size(R), P  Q, guard(T), Rplus?(x1), b, P  Q, x:A. B(x), False, , x(s)
Lemmas	finite-prob-space wf, bool wf, fpf wf, decl-type wf, decl-state wf, IdLnk wf, Knd wf, Id wf, rationals wf, Rplus wf, false wf, es realizer wf, Rplus-right wf, nat plus wf, Rplus-left wf, R-size wf, guard wf, Rplus? wf, assert wf, es realizer-induction